T:(IdType), tab:secret-table(T), x:Atom1.
isl(st-lookup(tab;x))  (n:||tab|| . nptr(tab) & st-atom(tab;n) = x) 

latex

Definitions	x:A. B(x), st-lookup(tab;x), ||tab|| , ptr(tab), st-atom(tab;n), let x,y,z = a in t(x;y;z), 1of(t), 2of(t), t  T, P  Q, {i..j}, p  q, true, P  Q, Prop, P & Q, P  Q, if b t else f fi, false, T, True, x. t(x), i  j < k, x:A. B(x), b, secret-table(T), , , Unit, x(s),
Lemmas	secret-table wf, Id wf, mu wf, bool wf, iff transitivity, assert wf, le wf, eqtt to assert, assert of le int, bor wf, btrue wf, lt int wf, bnot wf, eqff to assert, squash wf, true wf, bnot of le int, assert of lt int, eq atom wf1, pi1 wf, le int wf, bnot of lt int